Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    filter(cons(X,Y),0,M)  → cons(0,filter(Y,M,M))
2:    filter(cons(X,Y),s(N),M)  → cons(X,filter(Y,N,M))
3:    sieve(cons(0,Y))  → cons(0,sieve(Y))
4:    sieve(cons(s(N),Y))  → cons(s(N),sieve(filter(Y,N,N)))
5:    nats(N)  → cons(N,nats(s(N)))
6:    zprimes  → sieve(nats(s(s(0))))
There are 8 dependency pairs:
7:    FILTER(cons(X,Y),0,M)  → FILTER(Y,M,M)
8:    FILTER(cons(X,Y),s(N),M)  → FILTER(Y,N,M)
9:    SIEVE(cons(0,Y))  → SIEVE(Y)
10:    SIEVE(cons(s(N),Y))  → SIEVE(filter(Y,N,N))
11:    SIEVE(cons(s(N),Y))  → FILTER(Y,N,N)
12:    NATS(N)  → NATS(s(N))
13:    ZPRIMES  → SIEVE(nats(s(s(0))))
14:    ZPRIMES  → NATS(s(s(0)))
The approximated dependency graph contains 3 SCCs: {7,8}, {12} and {9,10}.
Tyrolean Termination Tool  (0.06 seconds)   ---  May 4, 2006